es:ES, i, x, y, z:Id, Tx, Ty, Tz:Type, P:(TxTyTzProp), Lx, Ly, Lz:Knd List.
es-frame(es;i;Lx;x;Tx)
 es-frame(es;i;Ly;y;Ty)
 es-frame(es;i;Lz;z;Tz)
 e@i.
 (kind(e)  Lx @ Ly @ Lz)
  P(x when e,y when e,z when e)
  P((x after e),(y after e),(z after e))
 @i stable state.P(state.x,state.y,state.z)   

latex

Definitions

hd(l), i<j, ij, l[i], ES, t  T, type List, x:A. B(x), E, left+right, P  Q, P  Q, x:AB(x), A, ij, ||as||, a<b, Case b of inl(x)  s(x) ; inr(y)  t(y), kind(e), s = t, A & B, x:A. B(x), A/x,y. B(x;y), 1of(t), x:AB(x), Void, x:A. B(x), Top, AtomFree(T;x), tag(k), lnk(k), isrcv(k), let x = a in b(x), when-after(e;info;pred?;init;Trans;val), state_when(e), outr(x), act(k), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), Msg(M), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), source(l), SWellFounded(R(x;y)), destination(l), loc(e), "$token", outl(x), pred(e), isl(x), first(e), pred!(e;e'), if a=b c ; d fi, i=j, rel_exp(T;R;n), x f y, , R^+, e < e', link(e), *, , sender(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv?(e), EOrderAxioms(E; pred?; info), Unit, , EqDecider(T), Atom$n, Id, IdLnk, es_info(es), <a,b>, inl(x), rcv(l,tg), 2of(t), inr(x), locl(a), tl(l), n-m, if a<b c ; d fi, b, if b t else f fi, nth_tl(n;as), n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), x.A(x), Y, AB, , {x:A| B(x) }, , car.cdr, x(s1,s2,s3), Prop, P  Q, P & Q, P  Q, False, x when e, (x after e), f(a), Type, Dec(P), e@i. P(e), {T}, SQType(T), s ~ t, vartype(i;x), loc(e), @i stable state.P(state)  , es-frame(es;i;L;x;T), x. t(x), Knd, as @ bs, kind(e), (x  l)

Lemmas

decidable or, alle-at wf, es-frame wf, es-after wf, es-loc wf, es-when wf, Id wf, Id sq, decidable l member, decidable equal Kind, iff transitivity, or functionality wrt iff, member append, append wf, l member wf, es-kind wf, es-E wf, Knd wf, event system wf